D:dsys{i:l}, P:({es:ES{i}| d-es{i:l}(D; es) }Prop{i'}).
d-realizes2{i:l}(D; es.P(es))  Prop{i''} 

latex

Definitions	x:A. B(x), P & Q, D realizes2 es.P(es), World, FairFifo, P  Q, PossibleWorld(D;w), x(s), ES(the_w), ES, es is an event system of D, x:A. B(x), Prop, t  T, Dsys
Lemmas	dsys wf, d-es wf, event system wf, w-es wf, possible-world wf, fair-fifo wf, world wf